This invention relates to system specification reduction methods.
One common method for dealing with the intrinsically intractable computational complexity of model-checking asynchronous systems is partial order reduction. This reduction technique exploits the common practice of modeling concurrent events in asynchronous systems as an interleaving of the events in all possible execution orders. An important observation about such systems is that often the properties one needs to check do not distinguish among these different orders. The reduction algorithm produces a state graph which contains only a subset of the states and transitions of the original system, but which contains enough information about the modeled system so that it is possible to apply model-checking algorithms to it instead of the full state graph. The verified property is guaranteed to be true in the reduced model if and only if it is true in the original model.
Since partial order reduction is naturally defined for asynchronous systems, it has thus far been applied mainly to the verification of software. Traditional partial order reduction algorithms use an explicit state representation, and a depth-first search. In contrast, other techniques for model checking, most notably symbolic model checking based on binary decision diagrams (BDDs), have proved most effective for synchronous systems, in particular for verifying hardware.
Previous implementations of partial order reduction algorithms in pre-existing state space search engines required considerable changes in the search mechanism. See, for example, P. Godefroid and D. Pirottin, "Refining Dependencies Improves Partial Order Verification Methods," Proc. 5.sup.th Conference on Computer Aided Verification, vol. 697 of Lecture Notes in Computer Science, pp. 438-449, Elounda, June 1993, Springer-Verlag, and G. J. Holzmann and D. Peled "An Improvement in Formal Verification," Formal Description Techniques 1994, pp. 197-211, Bern Switzerland, 1994, Chapman & Hall. The alternative was to construct a special tool for performing the search, for example, as described by A. Valmari in "A Stubborn Attack on State Explosion," Proc. 2.sup.nd Workshop on Computer Aided Verification, vol. 531 of Lecture notes in Computer Science, pp. 156-165, Rutgers, June, 1009, Springer-Verlag. [14]. In the Holtzman and Peled article, a reduction that is based on doing a large part of the calculations at compile time is described. However, some changes are still made to the search engine, controlling the backtracking mechanism in the depth-first search performed in the SPIN model checker, which is described by G. J. Holzmann in Design and Validation of Computer Protocols, Prentice Hall, 1992.
D. Peled described a simplified "ample sets" search method in "Combining Partial Order Reductions With on-the-fly Model Checking," Formal Methods In System Design, 8:39-64, 1996. This approach basically contemplates translating the specification into an internal code and then verifying the code with a model-checking tool that includes partial order reduction. The ample sets are the sets of transitions of the reduced graph that still describes the system. Since the notions of "ample sets" are employed in the instant disclosure, this article is hereby incorporated by reference. Closely related to this article is U.S. Pat. No. 5,615,137, issued to Holzmann and Peled on Mar. 25, 1997, and it, too, is hereby incorporated by reference.
In this prior art approach, a generator for the reduced model is created by appending a set of rules to the generator of the original model which, at least in part, are applied in the course of the model checking.
It is an object of this invention to create a set of rules that are applied as a transformation of the original model, and completely independently of the model checking or verification.
It is another object of this invention to create a generator that statically produces a reduced state graph.
It is another object of this invention to create a process that efficiently verifies the design of systems that include both software and hardware, and is well adapted to symbolic model checking.
It is still another object of this invention to create a process that is independent of the type of search employed, and is applicable to a depth-first search approach or a breadth-first search approach without a change.
It is yet another object of this invention to create a process that is compatible with existing model checking tools without requiring a change to their search engines.